Example 4.7.56 in [Borralleras - PhD'03]

Summary: Ex4_7_56_Bor03

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (Extra variables)
• Positive results:
  1. CSMSPO
  2. Zantema's transformation (LPO @ AProVE)
  3. Ferreira and Ribeiro's transformation (LPO @ AProVE)
  4. Giesl and Middeldorp's transformation (Corollary)
  5. VCSMSPO
  6. Polynomial ordering (MuTerm)
  7. CSRPO

CS-TRS Ex4_7_56_Bor03 (file Ex4_7_56_Bor03.csr)

Functions:  from cons s after 0

Constructors:  cons s 0

Variables:  X XS N

Arities: 

ar(from) = 1
ar(cons) = 2
ar(s) = 1
ar(after) = 2
ar(0) = 0

Replacement map: 

µ(from)={1}
µ(cons)={1}
µ(s)={1}
µ(after)={1,2}
µ(0)={}

Rules: (file Ex4_7_56_Bor03) 

from(X) -> cons(X,from(s(X)))
after(0,XS) -> XS
after(s(N),cons(X,XS)) -> after(N,XS)

The CS-TRS in OBJ format (file Ex4_7_56_Bor03.obj):

obj Ex4_7_56_Bor03 is
  sort S .
  op from : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op s : S -> S .
  op after : S S -> S .
  op 0 : -> S .
  vars X XS N : S .
  eq from(X) = cons(X,from(s(X))) .
  eq after(0,XS) = XS .
  eq after(s(N),cons(X,XS)) = after(N,XS) .
endo

Negative results

1. The µ-termination of Ex4_7_56_Bor03 cannot be proved by using Lucas' transformation: The TRS Ex4_7_56_Bor03_L:

       from(X) -> cons(X)
       after(0,XS) -> XS
       after(s(N),cons(X)) -> after(N,XS)
       

   contains extra variables.

Positive results

1. The µ-termination of Ex4_7_56_Bor03 can be proved by using Zantema's transformation. The TRS Ex4_7_56_Bor03_Z:

        from(X) -> cons(X,n__from(s(X)))
        after(0,XS) -> XS
        after(s(N),cons(X,XS)) -> after(N,activate(XS))
        from(X) -> n__from(X)
        activate(n__from(X)) -> from(X)
        activate(X) -> X
        

   is terminating (use LPO with AProVE).
2. The µ-termination of Ex4_7_56_Bor03 can also be proved by using Ferreira and Ribeiro's transformation. The TRS Ex4_7_56_Bor03_FR:

        from(X) -> cons(X,n__from(n__s(X)))
        after(0,XS) -> XS
        after(s(N),cons(X,XS)) -> after(N,activate(XS))
        from(X) -> n__from(X)
        s(X) -> n__s(X)
        activate(n__from(X)) -> from(activate(X))
        activate(n__s(X)) -> s(activate(X))
        activate(X) -> X
        

   is terminating. (use LPO with AProVE).
3. By [GM04, Theorem 22], the µ-termination of Ex4_7_56_Bor03 can also be proved by using Giesl and Middeldorp's transformation (but no concrete proof has been reported yet).
4. The µ-termination of Ex4_7_56_Bor03 is proved in [Bor03, Example 4.7.56] by using VCSMSPO.
5. The µ-termination of Ex4_7_56_Bor03 can also be proved by using a polynomial interpretation:

        [from](x) = 2x + 2
        [cons](x,y) = x + y/4
        [s](x) = 2x
        [after](x,y) = (x^2)y + 1
        [0] = 1
        

   See also the polynomial interpretation computed by MuTerm.
6. The µ-termination of Ex4_7_56_Bor03 can be proved by using CSRPO (proof due to Albert Rubio) and automatically by MuTerm :
   • marking map:

     	m(cons,2)={from}
     	

   • precedence:

     	from > cons, from', s
     	after > from 
     	

   • status:

     	st(after) = lex